Inference at * 2 
Iof proof for Lemma multiply nat wf:

.....set predicate..... NILNIL

1. i : 
2. j : 
  0  (i * j) 

latex

 by InteriorProof ((NatInd 2) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
CollapseTHEN ((Aut),(first_nat 3:n)) (first_tok SupInf:t) inil_term))) 

latex

C.

Definitions	i  j , False, A, A  B, P  Q, t  T, x:A. B(x), ,
Lemmas	ge wf, nat properties